Left Termination of the query pattern
max_valued(g,a)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 CutEliminatorProof (⇒, 0 ms)
↳2 Prolog
↳3 UndefinedPredicateHandlerProof (⇒, 0 ms)
↳4 Prolog
↳5 PrologToPiTRSProof (⇒, 0 ms)
↳6 PiTRS
↳7 DependencyPairsProof (⇔, 0 ms)
↳8 PiDP
↳9 DependencyGraphProof (⇔, 0 ms)
↳10 TRUE

(0) Obligation:

Clauses:

max_valued(.(Head, Tail), Max) :- max_Valued(Tail, Head, Max).
max_valued([], Term, Term).
max_valued(.(Head, Tail), Term, Max) :- ','(higher_valued(Head, Term), ','(!, max_valued(Tail, Head, Max))).
max_valued(.(Head, Tail), Term, Max) :- ','(higher_valued(Term, Head), max_valued(Tail, Term, Max)).
higher_valued(X, Y) :- greater(s(X), Y).
greater(s(X1), 0).
greater(s(X), s(Y)) :- greater(X, Y).

Query: max_valued(g,a)

(1) CutEliminatorProof (SOUND transformation)

Eliminated all cuts by simply ignoring them[PROLOG].

(2) Obligation:

Clauses:

max_valued(.(Head, Tail), Max) :- max_Valued(Tail, Head, Max).
max_valued([], Term, Term).
max_valued(.(Head, Tail), Term, Max) :- ','(higher_valued(Head, Term), max_valued(Tail, Head, Max)).
max_valued(.(Head, Tail), Term, Max) :- ','(higher_valued(Term, Head), max_valued(Tail, Term, Max)).
higher_valued(X, Y) :- greater(s(X), Y).
greater(s(X1), 0).
greater(s(X), s(Y)) :- greater(X, Y).

Query: max_valued(g,a)

(3) UndefinedPredicateHandlerProof (SOUND transformation)

Added facts for all undefined predicates [PROLOG].

(4) Obligation:

Clauses:

max_valued(.(Head, Tail), Max) :- max_Valued(Tail, Head, Max).
max_valued([], Term, Term).
max_valued(.(Head, Tail), Term, Max) :- ','(higher_valued(Head, Term), max_valued(Tail, Head, Max)).
max_valued(.(Head, Tail), Term, Max) :- ','(higher_valued(Term, Head), max_valued(Tail, Term, Max)).
higher_valued(X, Y) :- greater(s(X), Y).
greater(s(X1), 0).
greater(s(X), s(Y)) :- greater(X, Y).
max_Valued(X0, X1, X2).

Query: max_valued(g,a)

(5) PrologToPiTRSProof (SOUND transformation)

We use the technique of [TOCL09]. With regard to the inferred argument filtering the predicates were used in the following modes:
max_valued_in: (b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

max_valued_in_ga(.(Head, Tail), Max) → U1_ga(Head, Tail, Max, max_Valued_in_gga(Tail, Head, Max))
max_Valued_in_gga(X0, X1, X2) → max_Valued_out_gga(X0, X1, X2)
U1_ga(Head, Tail, Max, max_Valued_out_gga(Tail, Head, Max)) → max_valued_out_ga(.(Head, Tail), Max)

The argument filtering Pi contains the following mapping:
max_valued_in_ga(x1, x2)  =  max_valued_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x4)
max_Valued_in_gga(x1, x2, x3)  =  max_Valued_in_gga(x1, x2)
max_Valued_out_gga(x1, x2, x3)  =  max_Valued_out_gga
max_valued_out_ga(x1, x2)  =  max_valued_out_ga

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(6) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

max_valued_in_ga(.(Head, Tail), Max) → U1_ga(Head, Tail, Max, max_Valued_in_gga(Tail, Head, Max))
max_Valued_in_gga(X0, X1, X2) → max_Valued_out_gga(X0, X1, X2)
U1_ga(Head, Tail, Max, max_Valued_out_gga(Tail, Head, Max)) → max_valued_out_ga(.(Head, Tail), Max)

The argument filtering Pi contains the following mapping:
max_valued_in_ga(x1, x2)  =  max_valued_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x4)
max_Valued_in_gga(x1, x2, x3)  =  max_Valued_in_gga(x1, x2)
max_Valued_out_gga(x1, x2, x3)  =  max_Valued_out_gga
max_valued_out_ga(x1, x2)  =  max_valued_out_ga

(7) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

MAX_VALUED_IN_GA(.(Head, Tail), Max) → U1_GA(Head, Tail, Max, max_Valued_in_gga(Tail, Head, Max))
MAX_VALUED_IN_GA(.(Head, Tail), Max) → MAX_VALUED_IN_GGA(Tail, Head, Max)

The TRS R consists of the following rules:

max_valued_in_ga(.(Head, Tail), Max) → U1_ga(Head, Tail, Max, max_Valued_in_gga(Tail, Head, Max))
max_Valued_in_gga(X0, X1, X2) → max_Valued_out_gga(X0, X1, X2)
U1_ga(Head, Tail, Max, max_Valued_out_gga(Tail, Head, Max)) → max_valued_out_ga(.(Head, Tail), Max)

The argument filtering Pi contains the following mapping:
max_valued_in_ga(x1, x2)  =  max_valued_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x4)
max_Valued_in_gga(x1, x2, x3)  =  max_Valued_in_gga(x1, x2)
max_Valued_out_gga(x1, x2, x3)  =  max_Valued_out_gga
max_valued_out_ga(x1, x2)  =  max_valued_out_ga
MAX_VALUED_IN_GA(x1, x2)  =  MAX_VALUED_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x4)
MAX_VALUED_IN_GGA(x1, x2, x3)  =  MAX_VALUED_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(8) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MAX_VALUED_IN_GA(.(Head, Tail), Max) → U1_GA(Head, Tail, Max, max_Valued_in_gga(Tail, Head, Max))
MAX_VALUED_IN_GA(.(Head, Tail), Max) → MAX_VALUED_IN_GGA(Tail, Head, Max)

The TRS R consists of the following rules:

max_valued_in_ga(.(Head, Tail), Max) → U1_ga(Head, Tail, Max, max_Valued_in_gga(Tail, Head, Max))
max_Valued_in_gga(X0, X1, X2) → max_Valued_out_gga(X0, X1, X2)
U1_ga(Head, Tail, Max, max_Valued_out_gga(Tail, Head, Max)) → max_valued_out_ga(.(Head, Tail), Max)

The argument filtering Pi contains the following mapping:
max_valued_in_ga(x1, x2)  =  max_valued_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x4)
max_Valued_in_gga(x1, x2, x3)  =  max_Valued_in_gga(x1, x2)
max_Valued_out_gga(x1, x2, x3)  =  max_Valued_out_gga
max_valued_out_ga(x1, x2)  =  max_valued_out_ga
MAX_VALUED_IN_GA(x1, x2)  =  MAX_VALUED_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x4)
MAX_VALUED_IN_GGA(x1, x2, x3)  =  MAX_VALUED_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(9) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 0 SCCs with 2 less nodes.

(10) TRUE